Step of Proof: sub-equality
11,40
postcript
pdf
Inference at
*
1
2
1
I
of proof for Lemma
sub-equality
:
1.
T
: Type
2.
P
:
T
3.
i
:
T
4.
u
:
T
5.
i
=
u
6.
P
(
u
)
7.
P
(
i
)
i
=
u
latex
by Trivial
latex
latex.
origin
i = u
by Trivial
i = u
by Trivial